Nuprl Lemma : Rinterface-Rplus
11,40
postcript
pdf
A
,
B
:Top.
Rinterface(
A
B
)
~
let
rec1
= Rinterface(
A
) in
let
rec1
let
rec2
= Rinterface(
B
) in
let
rec1
let
rec2
if Rnone?(
rec1
) then
rec2
if Rnone?(
rec2
) then
rec1
else
rec1
rec2
fi
latex
Definitions
t
T
,
Rinterface(
A
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
A, B:Top.
B)
T